package mac5789.phase;

import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.LinkedBlockingDeque;
import java.util.concurrent.ThreadPoolExecutor;
import java.util.concurrent.TimeUnit;

import mac5789.solver.MiniSatSolver;
import mac5789.solver.SatSolver;

/**
 * Experimento de mudança de fases.
 * @author lundberg
 *
 */
public class PhaseChangeExperiment {

	private static final Double TARGET = 0.5;

	private final SatisfiabilityMeasurer measurer;

	private final int variablesPerProblem;

	private final int clausesStart;

	private final int clausesEnd;

	private final int initialStep;


	public PhaseChangeExperiment(SatisfiabilityMeasurer measurer, int variablesPerProblem) {
		this.measurer = measurer;
		this.variablesPerProblem = variablesPerProblem;
		this.clausesStart = variablesPerProblem;
		this.clausesEnd = variablesPerProblem * 8;
		this.initialStep = variablesPerProblem;
	}

	public void execute() {
		Set<Range> answers = new HashSet<Range>();
		Set<Range> candidates = new HashSet<Range>();
		candidates.add(this.findInitialRange()); 
		while(!candidates.isEmpty()) {
			Range candidate = candidates.iterator().next();
			candidates.remove(candidate);
			for(Range narrowed : this.narrowRange(candidate)) {
				if(this.canNarrow(narrowed)) {
					candidates.add(narrowed);
				} else {
					answers.add(narrowed);
				}
			}
		}
		for(Range answer : answers) {
			print(String.format("Mudança de fase entre %s cláusulas (%s) e %s cláusulas (%s)"
					, answer.start(), measure(answer.start()), answer.end(), measure(answer.end())));
		}
	}

	private Range findInitialRange() {
		int start = clausesStart;
		int end;
		Range rangeWithPhaseChange = null;
		while(start < clausesEnd) {
			end = start + initialStep;
			Range candidate = new Range(start, end);
			if (phaseChangeWithinRange(candidate)) { 
				rangeWithPhaseChange = candidate;
			}
			start = end;
		}
		if(rangeWithPhaseChange == null) {
			throw new RuntimeException("Não foi encontrado intervalo candidato para efetuar busca da mudança de fase.");
		} else {
			return rangeWithPhaseChange;
		}
	}

	private boolean canNarrow(Range range) {
		return (range.end() - range.start()) > 1;
	}

	private List<Range> narrowRange(Range range) {
		int middleNClauses = (range.end() - range.start())/2 + range.start();
		Range lower = new Range(range.start(), middleNClauses);
		Range middle = new Range(middleNClauses, middleNClauses);
		Range upper = new Range(middleNClauses, range.end());
		if(phaseChangeWithinRange(middle)) {
			return Arrays.asList(lower, middle, upper);
		} else if (phaseChangeWithinRange(lower)) {
			return Arrays.asList(lower);
		} else {
			return Arrays.asList(upper);
		}
	}

	private boolean phaseChangeWithinRange(Range candidate) {
		return measure(candidate.start()) <= TARGET && measure(candidate.end()) >= TARGET || measure(candidate.end()) <= TARGET && measure(candidate.start()) >= TARGET;
	}

	private double measure(int clauses) {
		return measurer.measure(variablesPerProblem, clauses);
	}

	private void print(String msg) {
		System.out.println(msg);	
	}

	private static class Range {
		private final int start;
		private final int end;
		public Range(int start, int end) {
			super();
			this.start = start;
			this.end = end;
		}
		public int start() {
			return start;
		}
		public int end() {
			return end;
		}
	}
}
